Warn people to not edit generated files.

diff --git a/mkstyle.sh b/mkstyle.sh
index 2df86c82b48dc6144f4f9f79bed597fee285444e..52c799a5c37dbe1e040ff4827f0ef8aa197b939e 100755 (executable)
--- a/mkstyle.sh
+++ b/mkstyle.sh
@@ -1,4 +1,8 @@
 
+echo "/* This file is machine-generated from the contents of style/ */"
+echo "/* by mkstyle.sh.   Editing it by hand is an exeedingly bad idea. */"
+echo 
+
 for i in style/*.style
 do
        A=`basename $i | sed "s/.style$//"`